T:Type, eq:(TT), f:(T), x:T, p:, q:. frequency(f;x) ~ (p/q)  Prop 

latex

Definitions	Type, t  T, , x:AB(x), , , #$n, a<b, P  Q, False, A, AB, , {x:A| B(x) }, x:A. B(x), n+m, {i..j}, P & Q, i  j < k, #{i<j|f i eq x}, |a/b - p/q| < 1/m, Prop, A & B, x:AB(x), x:A. B(x), frequency(f;x) ~ (p/q)
Lemmas	ratio-dist wf, seq-count wf, le wf, int seg wf, nat plus wf, nat wf, bool wf